An access control system enforces a policy that governs access to resources. For a given one or more principals (e.g., a user named “Joe”, a set of users in the group named “Group1”, etc.) and a given resource (e.g., a file named “foo.txt”, a file system, etc.), an access control system may determine whether the principal(s) can access the resource. In general, for a given request to access a resource, an access control system determines whether the access is allowed based on authenticated information about the principal(s) making the request.
One way to implement an access control policy is to specify it in a logic-based authorization language with constraints. In this approach, a policy is a set of rules written in such a language, and access requests are queries written in that language such that, given a particular set of facts, the requests can be determined to be true or false with respect to the policy and the facts. In a typical such language, a rule has a conclusion fact, zero or more conditional facts, and an optional constraint. The conclusion fact is deemed to be true if the conditional facts can be proven true. The purpose of the constraint is to restrict the possible values of variables occurring in the rule. A query succeeds if a proof tree can be constructed from the rules such that the conclusion of the proof tree is the query fact. The leaf nodes of such a proof tree are rules with zero conditional facts; in other words, they are known facts input to the query evaluation. For example, the fact “Joe can read foo.txt” may be a query that either succeeds (evaluates to true) or fails (evaluates to false), depending on whether the principal Joe is allowed to read foo.txt under the ambient policy and set of facts. The policy that governs access to foo.txt might say “X can read foo.txt if Administrator says X can read foo.txt”. If the policy also contains the fact “Administrator says Joe can read foo.txt”, the query is true under the policy, so Joe would be granted access. The Security Policy Assertion Language (SecPAL) is an example of a system that uses formal logical rules and constraints to model access policies and decisions, although there are other systems and languages that can be used to implement access policies with this model.
Modeling access control using constrained logic-based authorization languages leverages the power of formal logic to support complex access policies. However, a price of this power is that a policy can be implemented that is so complex that it may be hard for a human to predict its consequences. Ensuring that a principal has the security credentials that lead to the conclusion that the principal has permission to access a given resource, or debugging an access failure, can be difficult. Such tasks may involve adding, removing or analyzing the facts in the policy, i.e. the rules with no conditional facts that form the leaf nodes in proof trees. (The set of rules with conditional facts in the policy is typically much smaller than the set of facts in the policy, and is usually not frequently modified.) Thus one may wish to compute facts missing in the policy that would make a given query succeed.